COMMENT ⊗   VALID 00006 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	(DE SIFTUP(M V)
C00004 00003	tree ::= node|empty
C00006 00004	tree ::= node|termin
C00008 00005	version III
C00010 00006	version IV
C00012 ENDMK
C⊗;
(DE SIFTUP(M V)
    (COND
	((NO_SONS M) (STUFF M V))
	((TWO_SONS M) ((LAMBDA(Z)
				(COND
				   ((GREATERP (NODE Z) V)(PROG2(STUFF M (NODE Z))
							       (SIFTUP Z V))  )
				   (T(STUFF M V))))
			(COND
			   ((GREATERP (NODE(RIGHT M))(NODE (LEFT M))) (RIGHT M))
			   (T(LEFT M))) 
                       ))
	((ONE_SON M)((LAMBDA(Z)
			     (COND((GREATERP(NODE Z) V)(STUFF M (NODE Z))))
		      )(COND((EMPTY (LEFT M)) (RIGHT M))
			    (T(LEFT M)))))
))


(DE NO_SONS(M)(AND(EMPTY(LEFT M))(EMPTY(RIGHT M))))

(DE TWO_SONS(M)(NOT(OR (EMPTY(LEFT M))(EMPTY(RIGHT M)))))

(DE ONE_SON(M)(COND((EMPTY(LEFT M))(NOT(EMPTY(RIGHT M))))
		    (T (EMPTY(RIGHT M))) ))

(DE EMPTY(X)(NULL X))

(DE LEFT(X)(CAR X))
(DE RIGHT(X)(CADDR X))
(DE NODE(X)(CADR X))

(DE STUFF(X Y)(RPLACA(CDR X) Y))

(DE MK_NODE(X Y Z)(LIST X Y Z))


(SETQ L1(MK_NODE NIL 1 NIL))
(SETQ L2(MK_NODE NIL 2 NIL))
(SETQ L3(MK_NODE NIL 3 NIL))

(SETQ L(MK_NODE L1 2 L3))

(SETQ L4 (MK_NODE NIL 4 NIL))
(SETQ L5 (MK_NODE NIL 5 NIL))

(SETQ M (MK_NODE L4 1 L5))
(SETQ LL(MK_NODE M 2 L3))

FOO
tree ::= node|empty

node ::= struct[ tree:lb, number:value, tree:rb]

siftup[tree:m]tree
generic(m)
	[empty]       => LOSE
	[node(x,y,z)] => {generic(x,z)
				[empty,empty]       => m
				[empty,node(a,b,c)] => {y>b => T
							T => bugger(m,b) 
							     bugger(z,y)
							     siftup(z)}
				[node(a,b,c),empty] => {y>b =>T
							T => bugger(m,b)
							     bugger(x,y)
							     siftup(x)}
				[node(a,b,c),node(u,v,w)]
						=>{y>b∧y>v => T;
						   y>b → bugger(m,b)
							 bugger(x,y)
							 siftup(x);
						   T → bugger(m,u)
						       bugger(z,y)
						       siftup(y)}

			}


version I

input:
	m is tree
	lb and rb of m are ordered st. value at any descendant is ≤ value
	 at ancestor

output:
	siftup(m) is tree st. values are permutation of values of m
	m is ordered st value at any descendant is ≤ value at m.

bugger(x,y): x is a tree; the value at node x is changed to y.


tree ::= node|termin

node ::= struct[ tree:lb, number:value, tree:rb]
termin ::= number

siftup[tree:m]tree
generic(m)
	[termin]      => m
	[node(x,y,z)] => {generic(x,z)
				[termin,termin]     => {y≥x∧y≥z => m
							x>z =>exchange(y,x)
							T => exchange(y,z) }

				[termin,node(a,b,c)] => {y≥x∧y≥z => m
							 x≥z => exchange(x,y)
							 T => exchange(b,y)
								siftup(z);

				[node(a,b,c),termin] => {y≥x∧y≥z => m
							 z≥x =>exchange(z,y)
							T => exchange(b,y)
							     siftup(x)}
				[node(a,b,c),node(u,v,w)]
						=>{y>b∧y>v => T;
						   y>b → exchange(b,y)
							 siftup(x);
						   T → exchange(v,y)
						       siftup(z)}

			}


version II


version III
tree ::= node|termin

node ::= struct[ tree:lb, number:value, tree:rb]
termin ::= number

siftup[tree:m]tree
generic(m)
	[termin]      => m
	[node(x,y,z)] => {generic(x,z)
				[termin(b),termin(v)]     => {y≥b∧y≥v => m
							      b>v =>exchange(y,b)
							      T => exchange(y,v) }

				[termin(b),node(u,v,w)] => {y≥b∧y≥v => m
							    b≥v => exchange(y,b)
							    T => exchange(y,v)
								siftup(z);

				[node(a,b,c),termin(v)] => {y≥b∧y≥v => m
							    v≥b =>exchange(v,y)
							    T => exchange(b,y)
							     siftup(x)}
				[node(a,b,c),node(u,v,w)]
						=>{y>b∧y>v => m;
						   b≥v => exchange(b,y)
							 siftup(x);
						   T → exchange(v,y)
						       siftup(z)}

			}


version II

version IV
tree ::= node|termin

node ::= struct[ tree:lb, number:value, tree:rb]
termin ::= number

siftup[tree:m]tree
generic(m)
	[termin]      => m
	[node(x,y,z)] => siftup1(x,y,z)


siftup1[tree:x,number:y,tree:z]node
{generic(x,z)
	[termin(b),termin(v)]     => {y≥b∧y≥v => m
				      b>v =>exchange(y,b)
				      T => exchange(y,v) }

	[termin(b),node(u,v,w)] => {y≥b∧y≥v => m
				    b≥v => exchange(y,b)
				    T => exchange(y,v)
					siftup1(u,v,w);

	[node(a,b,c),termin(v)] => {y≥b∧y≥v => m
				    v≥b =>exchange(v,y)
				    T => exchange(b,y)
				     siftup1(a,b,c)}
	[node(a,b,c),node(u,v,w)]
			=>{y>b∧y>v => m;
			   b≥v => exchange(b,y)
				 siftup1(a,b,c);
			   T → exchange(v,y)
			       siftup1(u,v,w)}

			}


version II